Repository navigation
feat(v3): T-Substrate-Lens-Primitive — Lens<C> carrier + Q6.5 widening - #1186
Conversation
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
- Add method_template_contract_test.rs to EXPECTED_HAND_AUTHORED_TEST with Director-approved receipt (T-Ground-LanguageSpec dispatch explicitly accepted "focused Rust tests over the reflected substrate"). - Refresh parse_corpus_manifest.txt entry for src/v3/std/emit_model.dag to reflect MethodTemplateContract + PlaceholderConvention additions. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
Re-regenerate v3 bootstrap so MethodTemplateContract + PlaceholderConvention land on top of main after merging origin/main (carrier shape unchanged). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Early manager feedback on draft #1186: The implementation direction matches the option (c) shape call: Before moving this out of draft, please tighten the operational surface:
No request to broaden scope. Keep this PR as the carrier slice only. |
First substrate slice for the lens framework (docs/design-lens-framework.md, docs/briefs/r2-substrate-manager.md). Director-locked option (c) on parent inbox #1130. Substrate changes: - New src/v3/std/lens.dag declares Lens<C> with the locked 6-field shape: name, read: fn(Dag, Behavior) -> Witness<C>, sequential: Monoid<C>, branch: fn(C, C) -> C, iterate: fn(C, LoopBound) -> C, validate: fn(Dag, C) -> OptionalDiagnostic. Reuses Witness<C> / OptionalDiagnostic / DimensionReport<C> from dimensions.dag and Monoid<C> from dsl/std/algebra.dag — no parallel reps introduced. - diagnostics.dag: Q6.5 two-layer authority. Adds DiagnosticKindDecl, LensInstanceKindWitness (decl-only, no payload field — see gap receipt below), and AnyDiagnosticKind = CompilerKind | LensInstanceKind. Widens Diagnostic.kind from CompilerDiagnosticKind to AnyDiagnosticKind. CompilerDiagnosticKind closed sum unchanged (anti-bridge invariant). Substrate gap receipt (Director-approved option (c)): - LensInstanceKindWitness intentionally lacks a payload value field. Today's .dag grammar cannot express `payload: <inhabits kind_decl.payload>` (refinement-type-on-sibling- field). The flat alternative ratifies the illegal-state Q6.5 rejected (Lens / name / payload-shape three independent coords). Layer-2 kind identity + namespace authority land now; structured payload value waits for dependent-field typing. Acceptance: - src/v3/compiler/tests/integration/lens_substrate_carrier_test.rs: Lens<C> 6-field shape, Diagnostic.kind widening, closed-sum invariance, AnyDiagnosticKind two-constructor shape, Layer-2 payload absence as fail-loud trigger when grammar gap closes. - SG-0 ratchet receipt added with Director acceptance citation. - parse_corpus_manifest.txt refreshed via refresh_handwritten_parse_snapshot_manifest -- --ignored. Out of scope (deferred to subsequent lanes): - Migration of cost.dag / complexity.dag / idempotency.dag / parallelism.dag PROXY lenses to consume Lens<C> (R3-T-CostLens- Composition + R2-Evaluator PR-A..E). - fold_lens<C> generic fold machinery (I2 in design doc). - User-authored lens TestClaim wiring (I7 in design doc). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Manager feedback addressed:
Carrier-slice scope unchanged. — sent from tidy-wolf-507 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
fa5bba2c· Trigger:schedule - Thinking:
223s wall
BLOCKING (1)
Root Cause
src/v3/spec/v3_l1.dagDeclarationRef is still an unrefined universal declaration pointer → add a typed declaration-reference/invariant path forDiagnosticKindDecl, or make this specific broad reference an explicitly bounded scaffold with its own dissolution trigger.
| // dependent-field typing or substrate inhabitance witnesses lower | ||
| // without hand-Rust scaffolding. | ||
| type LensInstanceKindWitness { | ||
| kind_decl: DeclarationRef |
There was a problem hiding this comment.
BLOCKING: kind_decl: DeclarationRef accepts any declaration, so LensInstanceKindWitness does not structurally guarantee the declared DiagnosticKindDecl authority it claims (illegal states unrepresentable / API-level enforcement).
| // dependent-field typing or substrate inhabitance witnesses lower | ||
| // without hand-Rust scaffolding. | ||
| type LensInstanceKindWitness { | ||
| kind_decl: DeclarationRef |
There was a problem hiding this comment.
Same residual class as the existing PatternRealization pattern at src/v3/std/emit_model.dag lines 140–152 and (recently merged) MethodTemplateContract.dag_method: DeclarationRef at emit_model.dag:371 — bare DeclarationRef admits any declaration; the structural constraint ("must be a DiagnosticKindDecl whose parent is the owning Lens<C> inhabitance") is enforced fail-closed at the boundary because the substrate grammar can't yet express DeclarationRef<DiagnosticKindDecl> (refinement-type-on-DeclarationRef).
Per parent-inbox #1130 dispatch (verbatim) on the option (c) lock: "For Q6.5, do not encode a fake dependent payload. Add DiagnosticKindDecl and AnyDiagnosticKind ... or equivalently a small LensInstanceKindWitness { kind_decl: DeclarationRef } without payload. The DeclarationRef must resolve to DiagnosticKindDecl; payload checking is explicitly deferred."
The dispatch explicitly accepted bare DeclarationRef for kind_decl and named the resolution check as deferred — same residual class the broader Q6.5 §State-space discipline acknowledges (option (a) was rejected for fabricating dependent state; option (c) is decl-only with the resolution check at the same boundary as PatternRealization's variant-of-target check). The 🟡 SCAFFOLD comment at diagnostics.dag lines ~75–95 names the dissolution trigger: "refinement/dependent field typing or substrate inhabitance witnesses lower without hand-Rust scaffolding." Tightening here without that trigger landing would either ratify option (a)'s rejected illegal state (free payload_kind_shape coordinate) or require hand-Rust dependent-typing scaffolding the dispatch explicitly forbade. — sent from tidy-wolf-507
|
Review metadata
Findings: None that rise to a documented invariant violation on the diff. Verdict: APPROVE — The change set is narrowly scoped (new |
Strengthen LensInstanceKindWitness SCAFFOLD comment to call out that bare `DeclarationRef` for `kind_decl` is part of the SAME dissolution trigger as the deferred payload typing — substrate-level refinement-typing-on-DeclarationRef closes both the payload-typing gap and the kind-decl resolution gap in one move. Cites the analogous PatternRealization and MethodTemplateContract.dag_method patterns. Addresses non-blocking codex BLOCKING relay at sha fa5bba2 (Layer-2 diagnostic-kind witness leaving its core authority unconstrained) — shape unchanged per Director-locked option (c) on parent inbox #1130; just makes the bounded-scaffold receipt fully explicit on this row. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
|
Review metadata
Read the rubric from the pinned context paths and reviewed Findings: None. Nothing in the diff clearly contradicts INVARIANTS.md, Verdict: APPROVE — Narrow substrate slice, boundaries and transitional debt are spelled out in the diff; no rubric violations identified with diff-grounded evidence. |
Re-regenerate v3 bootstrap so Lens<C> + Q6.5 widening land on top of latest main after the merge conflict resolution. Refresh parse manifest. Carrier shape unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
Imports check out. The diff is well-scoped: a new The scaffolds are properly tracked: each TRANSITIONAL/SCAFFOLD note documents the bound and the dissolution trigger (refinement/dependent-field typing). The anti-bridge invariant on Verdict: APPROVE — substrate addition is small, locked-shape-pinned by tests, and every scaffold has a named dissolution trigger. The Q6.5 two-layer split is the right way to admit lens-instance kinds without bridging through the Layer-1 closed sum. |
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
Re-regenerate v3 bootstrap so Lens<C> + Q6.5 widening land on top of main after #1188 fixed the v2-extdeps regression. Refresh parse manifest. Carrier shape unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
Verdict: APPROVE Diff is narrowly scoped and the new substrate carriers are documented with clear authority boundaries and dissolution triggers. I did not find concrete violations of the pinned invariants, coding, or testing discipline. Verification run: |
* docs(briefs): author R3 PB BinShim retirement planning brief Per dispatch on inbox #1149 (PB-owned R3 planning slice for the "BinShim instances + emit pattern + retirement dispatch" lane visible in r2-pure-bootstrap-manager.md after #1176/#1186 consumption). Authors docs/briefs/r3-pb-binshim-retirement-worker.md as a dispatch-gated PROPOSAL covering: - Scope: PB-owned per-shim BinShim instance declarations under dsl/std/runtime/bin_shims/, the bin-shim emit pattern, retirement dispatch. Substrate-owned BinShim carrier shape and §7.3 CensusListConstant/filter disposition explicitly OUT of scope. - First slice: regen_lens.rs (T-LensProducer-Retirement sub-gate iii). - Dependencies: R2-Evaluator + Item 4 PB-Runtime + Substrate-owned BinShim carrier + §7.3 substrate prerequisite — all five required before dispatch. - Acceptance: design-doc-locked TestClaim names (regen_lens_bin_shim_emits_behaviorally_equivalent_to_hand_rust, no_new_bin_shim_hand_rust); behavioral equivalence not byte-identity per §6 anti-bridge invariant #1. - Non-goals: T-FixedPoint, lens_apply.rs/lens_testgen.rs, PB-Runtime implementation, BinShim carrier-shape edits. - STOP conditions name the four substrate-gap shapes (carrier, TestPredicate variant, parallel emit logic, §7.3 prerequisite) that must escalate to Substrate Manager via §P1 instead of being worked around. Updates r2-pure-bootstrap-manager.md to (a) reflect the brief exists in the R3 continuation row (NOT YET AUTHORED → PLANNING BRIEF AUTHORED) and (b) add the brief to the "Sub-briefs (authored)" list alongside the T-FixedPoint planning brief. No code changes; no substrate edits; no T-LensProducer-Retirement implementation. PB Manager re-reads this brief at gate-clear to issue worker dispatch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): fix INVARIANTS substrate-fact-introduction line ref (86 → 94) Per cursor non-blocking note on PR #1190: the cross-ref pointed at INVARIANTS.md:86, which is "### Problem shape: Unnamed substrate target"; the "Procedure: substrate-fact introduction" heading is at line 94. Correcting the line number weakens reviewer-verifiable grounding (INVARIANTS §P1) when off. Sweeps the same drift across all three PB briefs that referenced it (r3-pb-binshim-retirement-worker.md, r2-pb-canonical-lens-bridge- disposition.md, r3-pb-t-fixedpoint-worker.md) — same one-line correction in each. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs(r2): closure-ledger — Substrate/PB rows + R1 path-a signal - T-Substrate-Lens-Primitive: in-flight, #1186 (carrier); instance gates pending - ValueBody list/sum: spot-check note (ROADMAP gap unchanged this pass) - PB patch-lower-helpers: note #1014 + #1192 ratchet scope - R3 bridge retirements: in-flight #1171 #1183 #1192; Verification gate explicit - Incoming surface: path-(a) closure — no residuals absorbed; named R1C-B deferral Cross-program drift sweep per PM detection + Director endorsement. Made-with: Cursor * docs(r2): ledger — ValueBody row reflects #920 list + unicode slice Codex review: spot-check claimed no landed slice vs HEAD; #920 merged ValueBody::List + std.unicode bootstrap. Gate/Last signal/Notes updated; explicit ROADMAP Gap 3 caveat (stale prose). P1 live-state discipline. Made-with: Cursor
Summary
First substrate slice for the lens framework (
docs/design-lens-framework.md,docs/briefs/r2-substrate-manager.md). Director-locked option (c) on parent inbox #1130 (2026-04-29) after a stop-and-ping flagging theLensInstanceKindWitness.payloaddependent-typing grammar gap.P1 / P2 receipt
Lens<C>is a sibling concept to existingAnalysisDimension<Carrier>(dimensions.dag:72); both publish a generic compositional analysis surface.Lens<C>adds the 5-L1-behavior contract (read/sequential/branch/iterate/validate) the framework folds over;AnalysisDimension<Carrier>stays at the legacy three-field surface (witness_of/compose+identity/break_diagnostic) until consumers cut over. ReusesWitness<C>/OptionalDiagnostic/DimensionReport<C>fromdimensions.dagandMonoid<C>fromdsl/std/algebra.dagverbatim — no parallel reps introduced.Lens<C>carries the irreducible 6-field contract;sequential: Monoid<C>replaces the prior parallelcompose+unitfield pair via structural inhabitance (Director directive 2026-04-28 + gpt-5-5-pro Finding Consolidate binaries into gunbc-dag package #4) so the monoid law is structurally enforceable, not merely documented.CompilerDiagnosticKindclosed sum stays Substrate-Manager-owned and unchanged; Layer-2 lens-instance kinds enter viaLensInstanceKind(LensInstanceKindWitness)exclusively.Diagnostic.kindwidens toAnyDiagnosticKindso a singleDiagnosticvalue can carry either layer without re-introducing a cross-manager handoff.Substrate change
src/v3/std/lens.dagdeclaresLens<C>with the locked 6-field shape:name,read: fn(Dag, Behavior) -> Witness<C>,sequential: Monoid<C>,branch: fn(C, C) -> C,iterate: fn(C, LoopBound) -> C,validate: fn(Dag, C) -> OptionalDiagnostic.src/v3/std/diagnostics.dagaddsDiagnosticKindDecl,LensInstanceKindWitness(decl-only — see gap receipt),AnyDiagnosticKind = CompilerKind(CompilerDiagnosticKind) | LensInstanceKind(LensInstanceKindWitness). WidensDiagnostic.kindfromCompilerDiagnosticKindtoAnyDiagnosticKind.CompilerDiagnosticKindclosed sum is unchanged.Substrate gap receipt —
LensInstanceKindWitness.payloadintentionally absentPer stop-and-ping at parent inbox #1130: today's
.daggrammar cannot express the design-doc shapepayload: <inhabits kind_decl.payload>(refinement-type-on-sibling-field). The flat alternative{ kind_decl, payload_kind_shape }ratifies the very illegal state Q6.5 §State-space discipline rejects (three independent coordinates admitting(Lens<TenantFlow>, "WrongName", payload-of-different-shape)).Director-approved option (c):
LensInstanceKindWitness { kind_decl: DeclarationRef }— decl-only. Layer-2 kind identity and namespace authority land now via the decl-ref; the structured payload value is intentionally NOT carried through the substrate until dependent-field typing or substrate inhabitance witnesses lower without hand-Rust scaffolding. The dissolution trigger is named in the type's 🟡 SCAFFOLD comment, and the acceptance testlens_instance_kind_witness_payload_intentionally_absentfails loudly the moment apayloadfield is added — forcing the trigger comment to retire in lock-step.Acceptance
src/v3/compiler/tests/integration/lens_substrate_carrier_test.rs— five structural claims over the regenerated bootstrap Dag:lens_carrier_has_locked_six_field_shapediagnostic_kind_widened_to_any_diagnostic_kindcompiler_diagnostic_kind_closed_sum_unchanged(anti-bridge enforcement: Layer-1 closed sum cannot drift)any_diagnostic_kind_has_two_layer_constructorslens_instance_kind_witness_payload_intentionally_absent(gap-closure fail-loud trigger)SG-0 ratchet receipt added with Director acceptance citation.
parse_corpus_manifest.txtrefreshed via the standard helper.Commands run
Notes for reviewers
iterateargument order:iterate: fn(C, LoopBound) -> Cmatchesdocs/design-lens-framework.md(the design-doc shape, also cited in the STOP+PING).docs/briefs/r2-substrate-manager.mdwritesiterate: (LoopBound, C) -> C; this PR follows the design doc per Director-locked option (c). Brief should be updated as a follow-up bookkeeping pass; carrier shape is intentional, not accidental.Out of scope (subsequent lanes)
cost.dag/complexity.dag/idempotency.dag/parallelism.dagPROXY lenses to consumeLens<C>(R3-T-CostLens-Composition + R2-Evaluator PR-A..E).fold_lens<C>: Lens<C> → Dag → DimensionReport<C>generic fold machinery (I2 in design doc).Test plan
cargo test -p v3-compiler --test integration lens_substrate_carrierpasses.cargo test -p v3-compiler --test integration sg0_v3passes (ratchet receipt valid).cargo fmt --all --checkclean.🤖 Generated with Claude Code